Skip to content

Fe contains#145

Merged
ax0 merged 30 commits intomainfrom
fe-contains
Mar 27, 2025
Merged

Fe contains#145
ax0 merged 30 commits intomainfrom
fe-contains

Conversation

@tideofwords
Copy link
Collaborator

DRAFT

Add contains statements for frontend types:
DictContains
DictNotContains
SetContains
SetNotContains
ArrayContains

Work in progress -- will need to create duplicate frontend::Operation and middleware::Operation, and force the compiler to do the conversion.

Gt = 4,
Lt = 5,
Contains = 6,
NotContains = 7,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are these still needed?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nope! Removed them, thanks for pointing that out :)

arnaucube and others added 22 commits March 19, 2025 07:02
* merkletree: add keypath circuit

* merkletree-circuit: implement proof of existence verification in-circuit

* parametrize max_depth at the tree circuit

* Constrain selectors in-circuit

* implement merketree nonexistence proof circuit, and add edgecase tests

* add non-existence proofs documentation in the mdbook, mv EMPTY->EMPTY_VALUE & NULL->EMPTY_HASH, dependency clean and public exposure methods

* review comments, some extra polishing and add a test that expects wrong proofs to fail

* Add circuit to check only merkleproofs-of-existence

With this, the merkletree_circuit module offers two different circuits:
- `MerkleProofCircuit`: allows to verify both proofs of existence and proofs
non-existence with the same circuit.
- `MerkleProofExistenceCircuit`: allows to verify proofs of existence only.

In this way, if only proofs of existence are needed,
`MerkleProofExistenceCircuit` should be used, which requires less amount
of constraints than `MerkleProofCircuit`.

* Code review

---------

Co-authored-by: Ahmad <root@ahmadafuni.com>
* merkletree: add keypath circuit

* merkletree-circuit: implement proof of existence verification in-circuit

* parametrize max_depth at the tree circuit

* Constrain selectors in-circuit

* implement merketree nonexistence proof circuit, and add edgecase tests

* add non-existence proofs documentation in the mdbook, mv EMPTY->EMPTY_VALUE & NULL->EMPTY_HASH, dependency clean and public exposure methods

* review comments, some extra polishing and add a test that expects wrong proofs to fail

* Add circuit to check only merkleproofs-of-existence

With this, the merkletree_circuit module offers two different circuits:
- `MerkleProofCircuit`: allows to verify both proofs of existence and proofs
non-existence with the same circuit.
- `MerkleProofExistenceCircuit`: allows to verify proofs of existence only.

In this way, if only proofs of existence are needed,
`MerkleProofExistenceCircuit` should be used, which requires less amount
of constraints than `MerkleProofCircuit`.

* Code review

---------

Co-authored-by: Ahmad <root@ahmadafuni.com>
@tideofwords tideofwords changed the title DRAFT Fe contains Fe contains Mar 19, 2025
@tideofwords
Copy link
Collaborator Author

OK I think this is ready to merge. It does:

  • A Merkle proof is included as part of the "Operation" for a Contains or NotContains statement
  • Frontend Contains and NotContains predicates are replaced with different predicates for different frontend compound types (DictContains, ...)

@ed255 ed255 self-requested a review March 20, 2025 11:29
}

pub fn args(&self) -> Vec<Statement> {
pub fn args(&self) -> Vec<OperationArg> {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My suggestion would be to change this so that args still returns Vec<Statement>.
And instead of introducing an OperationArg, add a new method Operation::aux(&self) -> OperationAux which returns the auxiliary data of the operation.

enum OperationAux {
  None,
  MerkleProof(MerkleProof),
}

I think this would simplify things a bit.

Then on the frontend I would suggest doing something similar.

pub struct Operation(pub OperationType, pub Vec<OperationArg>, pub OperationAux);

And keep the frontend::OperationArg untouched.

And the same idea in mock_main

Copy link
Collaborator

@ed255 ed255 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've taken a quick look to see the changes related to this suggestion #145 (comment)
and this LGTM!

@tideofwords
Copy link
Collaborator Author

tideofwords commented Mar 25, 2025

(Responding to a question from a call this morning)

Why did I implement this new logic manual_compile_st_op() for DictContains (to introduce a ValueOf statement for EMPTY_VALUE), when we already have a method for converting literal statement arguments to ValueOf constants?

Because I want the literal to be introduced at a different time: I want it to be introduced only in the middleware pod statements, not in the frontend pod statements.

In other words: I want the frontend statements to contain a single statement
SetContains(root, val)
which the compiler converts to two middleware statements

ValueOf(empty_ak, EMPTY_VALUE)
Contains(root, val, empty_ak).

... Are you (@ax0 @ed255 @arnaucube) suggesting that I redesign it, so the frontend statements look like

ValueOf(empty_ak, EMPTY_VALUE)      // this now appears to be here for no reason at all
SetContains(root, val)

and the backend looks the same as before

ValueOf(empty_ak, EMPTY_VALUE)
Contains(root, val, empty_ak)?

I guess this would make the code simpler but the frontend pods would have an unexplained ValueOf statement...

@ed255
Copy link
Collaborator

ed255 commented Mar 26, 2025

We discussed the possibility of having a canonical hardcoded ValueOf statement with key=EMPTY_VALUE (or some other reserved key) and value=0. And then we can always assume this ValueOf statement exists and then turn DictContains(root, val) into Contains(root, val, (SELF, EMTPY_VALUE)) knowing that the EMPTY_VALUE statement will exist.

We also discussed merging this PR as is so that we can advance and keep the discussion open and resolve this later.

And while writing this I thought of a new solution: add frontend::NativePredicate::Contains and NotContains.
So the user creates operations of Dict, Set, Array and passes them to the builder, which in turn translates them into frontend Contains and NotContains with literals if necessary, and then these go through the process of moving away the literal into a ValueOf, all in the builder.
What I'm saying is that the frontend type contains the syntax sugar but also the underlying thing. And the user can use the syntax sugar at convenience, which is immedietaly converted to the underlying representation already with frontend types.

BTW shouldn't it be SetContains(root, v) -> Contains(root, v, empty_value)? and not DictContains?

@tideofwords
Copy link
Collaborator Author

tideofwords commented Mar 26, 2025

BTW shouldn't it be SetContains(root, v) -> Contains(root, v, empty_value)? and not DictContains?

yes, I fixed it :)

@tideofwords
Copy link
Collaborator Author

I won't be able to do much work on this for at least a couple days so... maybe just merge now and discuss later?

@ax0 ax0 merged commit d00ff95 into main Mar 27, 2025
4 checks passed
@ed255 ed255 mentioned this pull request Mar 31, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants